$\forall$${\it es}$:ES, $A$, $B$:Type, ${\it Ia}$:AbsInterface($A$), ${\it Ib}$, ${\it Ic}$:AbsInterface($B$), $f_{1}$:(E(${\it Ia}$)$\rightarrow$$B$).
\\[0ex](glued(${\it es}$; $B$; $f_{1}$; ${\it Ia}$; ${\it Ib}$) \& glued(${\it es}$; $B$; ($\lambda$$e$.${\it Ib}$($e$)); ${\it Ib}$; ${\it Ic}$)) $\Rightarrow$ glued(${\it es}$; $B$; $f_{1}$; ${\it Ia}$; ${\it Ic}$)